Rplus(${\it left}$; ${\it right}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr (inl $<$${\it left}$, ${\it right}$$>$ )